@inproceedings{GFuzz,
 author = {Godefroid, Patrice and Kiezun, Adam and Levin, Michael Y.},
 title = {Grammar-based whitebox fuzzing},
 booktitle = {Programming Language Design and Implementation},
 year = {2008},
 isbn = {978-1-59593-860-2},
 pages = {206--215},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1375581.1375607},
 doi = {10.1145/1375581.1375607},
 acmid = {1375607},
 keywords = {automatic test generation, grammars, program verification, software testing},
} 

@inproceedings{BERT,
  title = "BERT:  BEhavioral Regression Testing",
  booktitle = "Workshop on Dynamic Analysis",
  year = 2008,
  pages = "36--42",
  author = "Alessandro Orso and Tao Xie"
}

@inproceedings{RothUnder,
 author = {Staats, Matt and Hong, Shin and Kim, Moonzoo and Rothermel, Gregg},
 title = {Understanding user understanding: determining correctness of generated program invariants},
 booktitle = {International Symposium on Software Testing and Analysis},
 year = {2012},
 pages = {188--198}
}

@inproceedings{ISSTA12,
  author = "Alex Groce and Chaoqiang Zhang and Eric Eide and Yang Chen and John Regehr",
  title = "Swarm Testing",
  booktitle = "International Symposium on Software Testing and Analysis",
  year = 2012,
  pages = "78--88"
}

@inproceedings{PLDI13,
  author = "Yang Chen and Alex Groce and Chaoqiang Zhang and Eric Eide and John Regehr",
  title = "Taming Compiler Fuzzers",
  booktitle = "ACM SIGPLAN Conference on Programming Language Design and Implementation",
  year = 2013,
  note = "to appear"
}


@inproceedings{ExtInvar,
 author = {Alipour, Amin and Groce, Alex},
 title = {Extended program invariants: applications in testing and fault localization},
 booktitle = {Workshop on Dynamic Analysis},
 year = {2012},
 pages = {7--11},
 numpages = {5},
 url = {http://doi.acm.org/10.1145/2338966.2336799},
 doi = {10.1145/2338966.2336799},
 acmid = {2336799}
}

@inproceedings{ISSRE,
  author = "Alex Groce and Alan Fern and Jervis Pinto and Tim Bauer and Amin Alipour and Martin Erwig and Camden Lopez",
  title = "Lightweight Automated Testing with Adaptation-Based Programming",
  year = 2012,
  booktitle = "IEEE International Symposium on Software Reliability Engineering",
  note = "to appear"
}

@inproceedings{CFV2011,
  author = "Amin Alipour and Alex Groce",
  title = "Bounded Model Checking and Feature Omission Diversity",
  year = 2011,
  booktitle = "Workshop on Constraints in Formal Verification"
}

@inproceedings{OpAbs,
 author = {Harder, Michael and Mellen, Jeff and Ernst, Michael D.},
 title = {Improving test suites via operational abstraction},
 booktitle = {International Conference on Software Engineering},
 year = {2003},
 pages = {60--71}
} 



@inproceedings{MutRand,
  author = "Lu Zhang and Shan-Shan Hou and Jun-Jun Hu and Tao Xie and Hong Mei",
  title = "Is operator-based mutant selection superior to random mutant selection?",
  booktitle = "International Conference on Software Engineering",
  year = 2010,
  pages = "435--444"
}

@inproceedings{AdaptJava,
  author = "Tim Bauer and Martin Erwig and Alan Fern and Jervis Pinto",
  title = "Adaptation-based programming in {Java}",
  year = 2011,
  booktitle = "ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation",
  pages = "81--90"
}

@inproceedings{RobustAdapt,
  author = "Jervis Pinto and Alan Fern and Tim Bauer and Martin Erwig",
  booktitle = "International Conference on Machine Learning and Applications",
  year = 2010,
  title = "Robust Learning for Adaptive Programs by Leveraging Program Structure",
  pages = "943--948"
}

@inproceedings{ICSE12Feature,
  author = "N. Siegmund and S. S. Kolesnikov and C. Kastner and S. Apel and D. Batory and M. Rosenmuller and G. Saake",
  booktitle = "International Conference on Software Engineering",
  year = 2012,
  pages = "166--177",
  title = "Predicting Performance via Automated Feature-Interaction Detection"
}

@inproceedings{ProbSym,
 author = {Geldenhuys, Jaco and Dwyer, Matthew B. and Visser, Willem},
 title = {Probabilistic symbolic execution},
 booktitle = {International Symposium on Software Testing and Analysis},
 year = {2012},
 isbn = {978-1-4503-1454-1},
 location = {Minneapolis, MN, USA},
 pages = {166--176},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/2338965.2336773},
 doi = {10.1145/2338965.2336773},
 acmid = {2336773}
}

@inproceedings{BugRedux,
 author = {Jin, Wei and Orso, Alessandro},
 title = {{BugRedux}: reproducing field failures for in-house debugging},
 booktitle = {Int. Conf. on Software Engineering},
 year = {2012},
 isbn = {978-1-4673-1067-3},
 location = {Zurich, Switzerland},
 pages = {474--484},
 numpages = {11},
 url = {http://dl.acm.org/citation.cfm?id=2337223.2337279},
 acmid = {2337279},
} 


@article{Wilson,
  author = "E. B. Wilson",
  year = 1927,
  title = "Probable inference, the law of succession, and statistical inference",
  journal = "J. of the American Statistical Assoc.",
  volume = 22,
  pages = "209-212"
}


@article{stattest,
  author = "Simon Poulding and John A. Clark",
  title = "Efficient Software Verification: Statistical Testing Using Automated Search",
  journal = "IEEE Transactions on Software Engineering",
  volume = 36,
  issue = 6,
  year = 2010,
  pages = "763--777"
}

@article{searchtest,
  author = "Shaukat Ali and Lionel C. Briand and Hadi Hemmati and Rajwinder Kaur Panesar-Walawege",
  title = "A Systematic Review of the Application and Empirical Investigation of Search-Based Test Case Generation",
  journal = "IEEE Transactions on Software Engineering",
  volume = 36,
  issue = 6,
  year = 2010,
  pages = "742--762"
}

@article{structtest,
  author = "P. Thevenod-Fosse and H. Waeselynck",
  title = "An Investigation of Statistical Software Testing",
  journal = "J. Software Testing, Verification, and Reliability",
  volume = 1,
  number = 2,
  year = 1991,
  pages = "5--26"
}

@ARTICLE{McMinn04search-basedsoftware,
    author = {Phil McMinn},
    title = {Search-based Software Test Data Generation: A Survey},
    journal = {Software Testing, Verification and Reliability},
    year = {2004},
    volume = {14},
    pages = {105--156}
}

@inproceedings{Chen,
  title = "Fundamentals of test case selection: diversity, diversity, diversity",
  author = "Tsong Yueh Chen",
  year = 2010,
  booktitle = "International Conference on Software Engineering and Data Mining",
  pages = "723--724"
}

@inproceedings{ARTChen,
  author    = {Tsong Yueh Chen and
               Hing Leung and
               I. K. Mak},
  title     = {Adaptive Random Testing},
  booktitle = {Advances in Computer Science},
  year      = {2004},
  pages     = {320--329},
}

@inproceedings{ISSTAART,
  author = "Andrea Arcuri and Lionel Briand",
  title = "Adaptive Random Testing: An Illusion of Effectiveness",
  year = 2011,
  pages = "265--275",
  booktitle = "International Symposium on Software Testing and Analysis"
}

@inproceedings{FASE,
  author = "Rohan Sharma and Milos Gligoric and Andrea Arcuri and Gordon Fraser and Darko Marinov",
  title = "Testing Container Classes: Random or Systematic?",
  year = 2011,
  booktitle = "Fundamental Approaches to Software Engineering",
  pages = "262-277"
}

@inproceedings{Reinforce,
  author = "Margus Veanes and Pritam Roy and Colin Campbell",
  title = "Online Testing with Reinforcement Learning",
  year = 2006,
  booktitle = "Formal Approaches to Software Testing and Runtime Verification",
  pages = "240--253"
}

@inproceedings{HamletOnly,
   author = "Richard Hamlet",
   title = "When Only Random Testing Will Do",
   booktitle = "International Workshop on Random Testing",
   year = 2006,
   pages = "1--9"
}

@misc{NIST,
  author = "{NIST}",
  title = "{NIST} Covering Array Tables",
  howpublished = "\url{http://math.nist.gov/coveringarrays/ipof/tables/table.5.2.html}"
}

@misc{yaffs2,
  key = "Yaffs",
  title = "YAFFS: A Flash file system for embedded use",
  howpublished = "\url{http://www.yaffs.net/}"
}

@inproceedings{JavaPred,
  author = "C. Boyapati and Sarfraz Khurshid and Darko Marinov",
  title = "Korat:  Automated testing based on {Java} predicates",
  booktitle = "International Symposium on Software Testing and Analysis",
  year = 2004,
  pages = "195--205"
}

@inproceedings{MachCode,
  title = "Model Checking Machine Code with the {GNU} Debugger",
  year = 2005,
  booktitle = "SPIN Workshop on Model Checking Software",
  author = "Eric Mercer and Michael Jones"
}

@article{CoverArray,
 author = "J. F. Lawrence and R. N. Kacker and D. R. Kuhn and M. Forbes",
 title = "A Survey of Binary Covering Arrays",
 year = 2011,
 journal = "The electronic journal of combinatorics",
 volume = 18,
 number = "P84"
}

@article{TestEra,
  author = "Sarfraz Khurshid and Darko Marinov",
  title = "TestEra:  Specification-based testing of {Java} programs using {SAT}",
  journal = "Automated Software Engineering Journal",
  volume = 11,
  number = 4,
  year = 2004,
  pages = "403--434"
}

@book{JacksonBook,
  author = "Daniel Jackson",
  title = "Software Abstractions:  Logic, Language and Analysis",
  publisher = "The MIT Press",
  year = 2006
}

@inproceedings{Hybrid,
  author = "Rupak Majumdar and Koushik Sen",
  title = "Hybrid Concolic Testing",
  year = 2007,
  booktitle = "International Conference on Software Engineering",
  pages = "416--426"
}


@inproceedings{AndrewsL07,
  author    = {James Andrews and
               Felix Li and Tim Menzies},
  title     = {Nighthawk: A Two-Level Genetic-Random Unit Test Data Generator},
  booktitle = {Automated Software Engineering},
  pages = {144--153},
  year      = {2007}
}

@article{MeyerStateful,
  title = "Stateful Testing:  Finding more errors in code and contracts",
  year = 2011,
  author = "Yi Wei and Yu Pei and Hannes Roth and Alex Horton and Michael Steindorfer and Carlo A. Furia and Martin Nordio and Bertrand Meyer",
  journal = "Computing Research Repository",
  month = aug
}

@article{combin,
  title = "Software Fault Interactions and Implications for Software Testing",
  year = 2004,
  author = "D. Richard Kuhn and Dolores R. Wallace and Albert M. Gallo, Jr",
  journal = "IEEE Transactions on Software Engineering",
  volume = 30,
  number = 6,
  pages = "418--421"
}

@incollection{Hamlet94,
  author = {Richard Hamlet},
  title = {Random testing},
  booktitle = {Encyclopedia of Software Engineering},
  publisher = {Wiley},
  pages = {970--978},
  year = {1994},
}

@inproceedings{ClaessenH00,
  author    = {Koen Claessen and
               John Hughes},
  title     = {{QuickCheck}: a lightweight tool for random testing of Haskell
               programs},
  booktitle = {ICFP},
  year      = {2000},
  pages     = {268--279},
  ee        = {http://doi.acm.org/10.1145/351240.351266},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{PachecoE05,
  author    = {Carlos Pacheco and
               Michael D. Ernst},
  title     = {Eclat: Automatic Generation and Classification of Test Inputs},
  booktitle = {European Conference on Object-Oriented Programming},
  year      = {2005},
  pages     = {504--527},
  ee        = {http://dx.doi.org/10.1007/11531142_22},
  crossref  = {DBLP:conf/ecoop/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ecoop/2005,
  editor    = {Andrew P. Black},
  title     = {ECOOP 2005 - Object-Oriented Programming, 19th European
               Conference, Glasgow, UK, July 25--29, 2005, Proceedings},
  booktitle = {ECOOP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3586},
  year      = {2005},
  isbn      = {3-540-27992-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{SoftBET,
  title = "Software Assurance by Bounded Exhaustive Testing",
  author = "David Coppit and Jinlin Yang and Sarfraz Khurshid and Wei Le and Kevin Sullivan",
  journal = "IEEE Transactions on Software Engineering",
  year = 2005,
  volume = 31,
  number = 4,
  month = apr,
  pages = "328--339"
}

@article{CsallnerS04,
  author    = {Christoph Csallner and
               Yannis Smaragdakis},
  title     = {{JCrasher}: an automatic robustness tester for {Java}},
  journal   = {Softw., Pract. Exper.},
  volume    = {34},
  number    = {11},
  year      = {2004},
  pages     = {1025--1050},
  ee        = {http://dx.doi.org/10.1002/spe.602},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{CiupaLOM07,
  author    = {Ilinca Ciupa and
               Andreas Leitner and
               Manuel Oriol and
               Bertrand Meyer},
  title     = {Experimental assessment of random testing for object-oriented
               software},
  booktitle = {International Symposium on Software Testing and Analysis},
  year      = {2007},
  pages     = {84--94},
  ee        = {http://doi.acm.org/10.1145/1273463.1273476},
  crossref  = {DBLP:conf/issta/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issta/2007,
  editor    = {David S. Rosenblum and
               Sebastian G. Elbaum},
  title     = {Proceedings of the ACM/SIGSOFT International Symposium on
               Software Testing and Analysis, ISSTA 2007, London, UK, July
               9--12, 2007},
  booktitle = {ISSTA},
  publisher = {ACM},
  year      = {2007},
  isbn      = {978-1-59593-734-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{WhittakerT94,
  author    = {James A. Whittaker and
               Michael G. Thomason},
  title     = {A {Markov} Chain Model for Statistical Software Testing},
  journal   = {IEEE Transactions on Software Engineering},
  volume    = {20},
  number    = {10},
  year      = {1994},
  pages     = {812--824},
  ee        = {http://www.computer.org/tse/ts1994/e0812abs.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{NVersion,
  author = "Susan Brilliant and John Knight and Nancy Leveson",
  title = "The Consistent Comparison Problem in N-Version Software",
  journal = "IEEE Transactions on Software Engineering",
  volume = 15,
  number = 11,
  year = "1987",
  pages = "1481--1485"
}

@inproceedings{DBLP:conf/icse/CleveZ05,
  author    = {Holger Cleve and
               Andreas Zeller},
  title     = {Locating causes of program failures},
  booktitle = {ICSE},
  year      = {2005},
  pages     = {342--351},
  ee        = {http://doi.acm.org/10.1145/1062455.1062522},
  crossref  = {DBLP:conf/icse/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icse/2005,
  editor    = {Gruia-Catalin Roman and
               William G. Griswold and
               Bashar Nuseibeh},
  title     = {27th International Conference on Software Engineering (ICSE
               2005), 15--21 May 2005, St. Louis, Missouri, USA},
  booktitle = {ICSE},
  publisher = {ACM},
  year      = {2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{ModelChecking,
  author="Edmund M. Clarke and Orna Grumberg and Doron Peled",
  title="Model Checking",
  publisher="MIT Press",
  year="2000"}



@book{ZellerBook,
  author="Andreas Zeller",
  title="Why Programs Fail: A Guide to Systematic Debugging",
  publisher="Morgan Kaufmann",
  year="2005"}

@book{Petroski,
  author="Henry Petroski",
  title="To Engineer is Human:  The Role of Failure in Successful Design",
  publisher="St. Martin's Press",
  year="1985"}

@inproceedings{PathSlicing,
  author = "Ranjit Jhala and Rupak Majumdar",
  title = "Path Slicing",
  booktitle = "Programming Language Design and Implementation",
  year = "2005",
  pages = "38--47"
}

@inproceedings{vmcai08,
  author = "Alex Groce and Rajeev Joshi",
  title = "Extending Model Checking with Dynamic Analysis",
  booktitle = "International Conference on Verification, Model Checking, and Abstract Interpretation",
  year = 2008,
  pages = "142--156"
}

@inproceedings{ICSEDiff,
  author = "Alex Groce and Gerard Holzmann and Rajeev Joshi",
  title = "Randomized Differential Testing as a Prelude to Formal Verification",
  booktitle = "International Conference on Software Engineering",
  year = 2007,
  pages = "621--631"
}

@inproceedings{MinUnit,
  author = "Yong Lei and James H. Andrews",
  title = "Minimization of Randomized Unit Test Cases",
  booktitle = "International Symposium on Software Reliability Engineering",
  year = "2005",
  pages = "267--276"
}

@inproceedings{minisat,
  author = "Niklas Een and Niklas Sorensson",
  title = "An Extensible {SAT}-Solver",
  booktitle =    {Symposium on the Theory and Applications of Satisfiability Testing ({SAT})},
  year = "2003",
  pages = "502--518"
}

@inproceedings{DynamicAnalysis,
  author = "Thomas Ball",
  title = "The Concept of Dynamic Analysis",
  booktitle = "European Software Engineering Conference/Foundations of Software Engineering",
  year = "1999",
  pages = "216--234"
}

@inproceedings{RL1,
  author = "D. Andre and S. Russel",
  title = "State abstraction for programmable reinforcement learning agents",
  year = 2002,
  booktitle = "National Conference on Artificial Intelligence"
}


@inproceedings{Pacheco,
  author = "Carlos Pacheco and Shuvendu K. Lahiri and Michael D. Ernst and Thomas Ball",
  title = "Feedback-directed Random Test Generation",
  booktitle = "International Conference on Software Engineering",
  year = "2007",
  pages = "75--84"
}

@inproceedings{SlicePromela,
  author = "Lynette I. Millett and Tim Teitelbaum",
  title = "Slicing {Promela} and its Applications to Model Checking, Simulation, and Protocol Understanding",
  booktitle = "SPIN Workshop on Model Checking of Software",
  year = "1998",
  pages = "75--83"
}

@inproceedings{LogFilesArch,
  author = "Gerald Gannod and Shilpa Murthy",
  title = "Using Log Files to Reconstruct State-Based Software Architectures",
  booktitle = "WCRE'02 Workshop on Software Architecture Reconstruction",
  year = "2002"
}

@inproceedings{MBTraceChecking,
  author = "Yvonne Howard and Stefan Gruner and Andrew M. Gravell and Carla Ferreira and Juan Carlos Augusto",
  title = "Model-Based Trace-Checking",
  booktitle = "SoftTest: UK Software Testing Research Workshop II",
  year = "2003"
}

@inproceedings{LogAudit,
  author = "Muriel Roger and Jean Goubault-Larrecq",
  title = "Log Auditing through Model-Checking",
  booktitle = "IEEE Workshop on Computer Security Foundations",
  year = "2001",
  pages = "220"
}

@inproceedings{PSE,
  author = "Roman Manevich and Manu Sridharan and Stephen Adams and Manuvir Das and Zhe Yang",
  title = "{PSE:} explaining program failures via postmortem static analysis",
  booktitle = "Foundations of Software Engineering",
  year = "2004",
  pages = "63--72"
}



@book{FSP,
  author = "J. Magee and J. Kramer",
  title = "Concurrency:  State Models and {Java} Programs",
  publisher = "John Wiley and Sons",
  year="1999"
}

@inproceedings{chaff,
    author = "Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Linao Zhang and Sharad Malik",
    title = "{Chaff: Engineering an Efficient {SAT} Solver}",
    booktitle = "Design Automation Conference",
    year = "2001",
    pages = "530--535"
}

@inproceedings{AlpernSSA,
  author = "Bowen Alpern and Mark N. Wegman and F. Kenneth Zadeck",
  title = "Detecting Equality of Variables in Programs",
  booktitle = "Principles of Programming Languages",
  year=1988,
  pages={1--11}
}

@inproceedings{ParaSlice,
  author = "John Field and Ganesan Ramalingam and Frank Tip",
  title = "Parametric Program Slicing",
  booktitle = "Principles of Programming Languages",
  year=1995,
  pages={379--392}
}

@inproceedings{CBMCp,
  author = "Daniel Kroening and Edmund M. Clarke and Flavio Lerda",
  title = "A Tool for Checking {ANSI-C} Programs",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
  year = "2004",
  pages = "168--176"
}

@article{RL2,
  author = "S. Mahadevan",
  title = "Agent reward reinforcement learning: Foundations, algorithms, and empirical results",
  journal = "Machine Learning",
  volume = 22,
  number = 1,
  pages = "159--195",
  year = 1996
}


@inproceedings{QL1,
  author = "S. Bradtke and M. O. Duff",
  title = "Reinforcement learning methods for continuous-time {Markov} decison problems",
  pages = "393--400",
  year = 1995,
  booktitle = "Advances in neural information processing systems"
}

@article{Imposs,
  author = "C. Kaner",
  title = "The impossibility of complete testing",
  year = 1997,
  journal = "Software QA",
  volume = 4,
  number = 4,
  page = 28,
  note = "\url{http://www.kaner.com/pdfs/imposs.pdf}"
}

@book{ManMonth,
  author = "Frederick Brooks",
  title = "The Mythical Man-Month:  Essays on Software Engineering, 20th Anniversary Edition",
  year = 1995,
  publisher = {{Addison-Wesley Professional}}
}

@inproceedings{TestPlan,
  author = "Klaus Havelund and Alex Groce and Gerard Holzmann and Rajeev Joshi and Margaret Smith",
  title = "Automated Testing of Planning Models",
  booktitle = "Workshop on Model Checking and Artificial Intelligence",
  year = 2008,
  pages = "90--105"
}

@inproceedings{RuleBased,
  author = "Howard Barringer and Klaus Havelund and David Rydeheard and Alex Groce",
  title = "Rule Systems for Runtime Verification: A short tutorial",
  booktitle = "International Workshop on Runtime Verification",
  year = 2009
}

@inproceedings{exploit,
  author = "Alex Groce and Rajeev Joshi",
  title = "Exploiting Traces in Program Analysis",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
  year = "2006",
  pages = "379--393"
}

@inproceedings{CK03,
  author = "E. Clarke and D. Kroening",
  title = "Hardware Verification using {ANSI-C} Programs as a Reference",
  booktitle = { Asia and South Pacific Design Automation Conference (ASP-DAC) },
  year = "2003",
  pages = {308--311}
}

@inproceedings{KLEE,
  author = "Cristian Cadar and Daniel Dunbar and Dawson Engler",
  title = "{KLEE}:  Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs",
  booktitle = "Operating System Design and Implementation",
  year = 2008,
  pages = "209--224"
}

@inproceedings{RWSet,
  author = "Peter Boonstoppel and Cristian Cadar and Dawson Engler",
  title = "RWSet:  Attacking Path Explosion in Constraint-Based Test Generation",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
  year = 2008,
  pages = "351--366"
}

@inproceedings{CEGARExe,
  title = "Counterexample Guided Abstraction Refinement Via Program Execution",
  booktitle = "International Conference on Formal Engineering Methods",
  year = 2004,
  pages = "224--238",
  author = "Daniel Kroening and Alex Groce and Edmund M. Clarke"
}

@inproceedings{CKY03,
  AUTHOR    = { D. Kroening
                and E. Clarke
                and K. Yorav },
  TITLE     = { Behavioral Consistency of {C} and {Verilog} Programs Using Bounded Model Checking },
  BOOKTITLE = { Design Automation Conference (DAC) },
  YEAR      = { 2003 },
  PAGES     = { 368--371 },
  ISBN      = { 1-58113-688-9 },
}

@InProceedings{PBS,
  author =       {F. Aloul and A. Ramani and I. Markov and K. Sakallah},
  title =        {{PBS}: A backtrack search pseudo {Boolean} solver},
  booktitle =    {Symposium on the Theory and Applications of Satisfiability Testing ({SAT})},
  pages =        {346--353},
  year =         {2002}
  }


@inproceedings{ClarkeEmerson,
  author = "Edmund M. Clarke and E. Emerson",
  title = "The Design and Synthesis of Synchronization Skeletons Using Temporal Logic",
  booktitle = "Workshop on Logics of Programs",
  year = "1981",
  pages = "52--71"
}

@inproceedings{SifakisMC,
  author = "Jean-Pierre Queille and Joseph Sifakis",
  title = "Specification and verification of concurrent systems in {CESAR}",
  pages = "337--351",
  year = "1982",
  booktitle = "International Symposium on Programming"
}


@InProceedings{HardSlice,
  author =       {Edmund M. Clarke and Masahiro Fujita and Sreeranga P. Rajan and Thomas W. Reps and Subash Shankar and Tim Teitelbaum},
  title =        {Program Slicing of Hardware Description Languages},
  booktitle =    {Correct Hardware Design and Verification Methods (CHARME)},
  pages =        {298--312},
  year =         {1999}
  }


@book{
  kurshan,
  author = "R. P. Kurshan",
  title = "Computer-Aided Verification of Coordinating Processes: The Automata-
Theoretic Approach",
  publisher = "Princeton University Press",
  year = "1995"
}

@inproceedings{BMCThread,
    author = "Ishai Rabinovitz and Orna Grumberg",
    title = "Bounded Model Checking of Concurrent Programs",
    booktitle = "Computer-Aided Verification",
    pages = "82--97",
    year = "2005"
}

@inproceedings{CEGAR,
    author = "E. Clarke and O. Grumberg and S. Jha and Y. Lu and
 H. Veith",
    title = "Counterexample-Guided Abstraction Refinement",
    booktitle = "Computer-Aided Verification",
    pages = "154--169",
    year = "2000"
}


@book{TimeWarp,
  editor = "D. Sankoff and J. Kruskal",
  title = "Time Warps, String Edits, and Macromolecules:  the Theory and Practice of Sequence Comparison",
  publisher = "Addison Wesley",
  year = "1983"
}

@incollection{Wagner,
  author = "R. Wagner",
  title = "On the Complexity of the Extended String-to-String Correction Problem",
  booktitle = "Time Warps, String Edits, and Macromolecules:  the Theory and Practice of Sequence Comparison",
  year = "1983",
  editor = "D. Sankoff and J. Kruskal",
  publisher = "Oxford University Press"
}

@book{Gusfield,
  author = "D. Gusfield",
  title = "Algorithms on Strings, Trees, and Sequences:  Computer Science and Computational Biology",
  publisher = "Cambridge University Press",
  year = "1997"
}

@book{Durbin,
  author = "R. Durbin and S. Eddy and A. Krogh and G. Mitchison",
  title = "Biological sequence analysis:  Probabilistic models of proteins and nucleic acids",
  publisher = "Cambridge University Press",
  year = "1998"
}

@article{ModelCode,
  author = "Gerard Holzmann and Rajeev Joshi and Alex Groce",
  title = "Model driven code checking",
  journal = "Automated Software Engineering",
  volume = 15,
  number = "3--4",
  year = 2008,
  pages = "283--297"
}

@article{Galles,
  author = "D. Galles and J. Pearl",
  title = "Axioms of Causal Relevance",
  volume = "97",
  number = "1--2",
  journal = "Artificial Intelligence",
  pages = "9--43",
  year = "1997"
}

@article{PowerTen,
  author = "G. J. Holzmann",
  title = "The Power of Ten:  Rules for Developing Safety Critical Code",
  volume = "39",
  number = "6",
  journal = "IEEE Computer",
  pages = "95--97",
  month = jun,
  year = "2006"
}

@inproceedings{Spirit,
  author = "Glenn Reeves and Tracy Neilson",
  title = "The {Mars} {Rover} {Spirit} {Flash} Anomaly",
  booktitle = "IEEE Aerospace Conference",
  year = "2005"
}

@article{BanderaSlice,
  author = "John Hatcliff and Matthew B. Dwyer and Hongjun Zheng",
  title = "Slicing Software for Model Construction",
  volume = "13",
  number = "4",
  journal = "Higher-Order and Symbolic Computation",
  pages = "315--353",
  year = "2000"
}



@InProceedings{POPAD,
  author =	 {Akash Lal and Junghee Lim and Marina Polishchuk and
                  Ben Liblit},
  title =	 {Path Optimization in Programs and its Application to
                  Debugging},
  booktitle =	 {European Symposium on Programming},
  year =	 2006,
  pages = "246--263"
}

@inproceedings{DwyerSearch,
  author = "Matthew B. Dwyer and Sebastian G. Elbaum and Suzette Person and Ragul Purandare",
  title = "Parallel Randomized State-Space Search",
  booktitle = "International Conference on Software Engineering",
  year = 2007,
  pages = "3--12"
}

@inproceedings{Bogor,
  author = "Robby and Matthew Dwyer and John Hatcliff",
  title = "Bogor: An Extensible and Highly-Modular Model Checking Framework",
  year = 2003,
  booktitle = "European Software Engineering Conference / Symposium on the Foundations of Software Engineering",
  pages = "267--276"
}


@inproceedings{TACASSlice,
  author = "Matthew B. Dwyer and John Hatcliff and Matthew Hoosier and Venkatesh Prasad Ranganath and Robby and Todd Wallentine",
  title = "Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
  year = "2006",
  pages = "73--89"
}

@inproceedings{JADE,
  author = "C. Mateis and M. Stumptner and D. Wieland and F. Wotawa",
  title = "Model-Based Debugging of {Java} Programs",
  booktitle = "Workshop on Automatic Debugging",
  year = "2000"
}

@article{Reiter,
  author = "R. Reiter",
  title = "A theory of diagnosis from first principles",
  journal = "Artificial Intelligence",
  volume = "32",
  number = "1",
  year = "1987",
  pages = "57--95"
}

@inproceedings{CMC,
  author = "M. Musuvathi and D. Park and A. Chou and D. Engler and D. Dill",
  title = "{CMC:} {A} Pragmatic Approach to Model Checking Real Code",
  booktitle = "Symposium on Operating System Design and Implementation",
  year = "2002"
}

@article{SENAssert,
  author = "L. A. Clarke and D. S. Rosenblum",
  title = "A historical perspective on runtime assertion checking in software development",
  journal = "ACM SIGSOFT Software Engineering Notes",
  volume = "31",
  number = "3",
  year = "2006",
  month = may,
  pages = "25--37"
}

@inproceedings{BMC,
  author = "Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Yunshan Zhu",
  title = "Symbolic Model Checking without {BDDs}",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems", 
  year = "1999",
  pages = "193--207"
}

@inproceedings{ModelDriven,
  author = "Gerard Holzmann and Rajeev Joshi",
  title = "Model-Driven Software Verification",
  booktitle = "SPIN Workshop on Model Checking of Software",
  year = "2004",
  pages = "76--91"
}

@inproceedings{VeriSoft,
  author = "Patrice Godefroid",
  title = "VeriSoft: a tool for the automatic analysis of concurrent software",
  booktitle = "Computer-Aided Verification",
  year = 1997,
  pages = "172--186"
}


@inproceedings{StatDebug,
  author = "A. Zheng and M. I. Jordan and B. Liblit and M. Naik and A. Aiken",
  title = "Statistical Debugging:  Simultaneous Identification of Multiple Bugs",
  booktitle = "International Conference on Machine Learning",
  year = "2006"
}

@inproceedings{DesignTest,
  author = "B. Pettichord",
  title = "Design for Testability",
  booktitle = "Pacific Northwest Software Quality Conference",
  year = "2002",
  month = oct
}

@inproceedings{LearnAssume,
  author = "J. Cobleigh and D. Giannakopoulou and C. P\u{a}s\u{a}reanu",
  title = "Learning assumptions for compositional verification",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems", 
  year = "2003",
  pages = "331--346"
}

@inproceedings{Bandera,
  title = "Bandera:  Extracting Finite-State Models from Java Source Code",
  year = 2000,
  booktitle = "International Conference on Software Engineering",
  pages = "439--448",
  author = "James Corbett and Matthew Dwyer and John Hatcliff and Shawn Laubach and Corina S. Pasareanu and Hongjun Zheng"
}

@inproceedings{NuSMV,
  author = "A. Cimatti and E. Clarke and E. Giunchiglia and F. Giunchiglia and M. Pistore and M. Roveri and R. Sebastiani and A. Tacchella",
  title = "{NuSMV} 2: An {OpenSource} Tool for Symbolic Model Checking",
  booktitle = "Computer-Aided Verification",
  year = "2002",
  pages = "359--364"
}


@article{Lucas,
  author = "P. Lucas",
  title = "Analysis of Notions of Diagnosis",
  journal = "Artificial Intelligence",
  volume = "105",
  number = "1--2",
  pages = "295--343",
  year = "1998"
}

@article{Fuzz,
  author = "B. P. Miller and L. Fredriksen and B. So",
  title = "An Empirical Study of the Reliability of {UNIX} Utilities",
  journal = "Communications of the ACM",
  volume = "105",
  number = "33(12)",
  pages = "32--44",
  year = "1990"
}

@inproceedings{TreeLike,
  author = "E. Clarke and S. Jha and Y. Lu and H. Veith",
  title = "Tree-Like Counterexamples in Model Checking",
  booktitle = "IEEE Symposium on Logic in Computer Science",
  year = "2002"
}

@book{Hume1,
  author = "D. Hume",
  title = "A Treatise of Human Nature",
  publisher = "London",
  year = "1739"
}

@book{Hume2,
  author = "D. Hume",
  title = "An Enquiry Concerning Human Understanding",
  publisher = "London",
  year = "1748"
}

@book{CausationBook,
  editor = "E. Sosa and M. Tooley",
  title = "Causation",
  publisher = "Oxford University Press",
  year = "1993"
}

@inproceedings{Qadeer,
  author = "Shaz Qadeer and Jakob Rehof",
  title = "Context-Bounded Model Checking of Concurrent Software",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
  month = apr,
  year=2005,
  pages={93--107}
}


@article{MackieCause,
  author = "J. Mackie",
  title = "Causes and Conditions",
  journal = "American Philosophical Quarterly",
  volume = "2",
  year = "1965",
  pages = "245--264"
}

@incollection{Stalnaker,
  author = "R. Stalnaker",
  title = "A Theory of Conditionals",
  booktitle = "Studies in Logical Theory",
  year = "1968",
  editor = "N. Rescher",
  publisher = "Oxford University Press"
}


@article{ProbCause,
  author = "W. Salmon",
  title = "Probabilistic Causality",
  journal = "Pacific Philosophical Quarterly",
  volume = "61",
  year = "1980",
  pages = "50--74"
}

@article{LewisCause,
  author = "D. Lewis",
  title = "Causation",
  journal = "Journal of Philosophy",
  volume = "70",
  year = "1973",
  pages = "556--567"
}

@article{KimCause,
  author = "J. Kim",
  title = "Causes and Counterfactuals",
  journal = "Journal of Philosophy",
  volume = "70",
  year = "1973",
  pages = "570--572"
}

@inbook{HorwichCause,
  author = "P. Horwich",
  title = "Asymmetries in Time",
  year = "1987",
  pages = "167--176"
}

@book{Counterfactuals,
  author = "D. Lewis",
  title = "Counterfactuals",
  publisher = "Harvard University Press",
  year = "1973 [revised printing 1986]"
}

@inproceedings{SPIN03,
  author = "A. Groce and W. Visser",
  title = "What Went Wrong:  Explaining Counterexamples",
  booktitle = "SPIN Workshop on Model Checking of Software",
  year = "2003",
  pages = "121--135"
}


@inproceedings{GroceDist,
  author = "Alex Groce",
  title = "Error Explanation with Distance Metrics",
  year = 2004,
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
  pages = "108--122"
}

@inproceedings{groce-structural,
  author = "Alex Groce and Willem Visser",
  title = "Model Checking Java Programs using Structural Heuristics",
  booktitle = "International Symposium on Software Testing and Analysis",
  year = "2002",
  pages = "12--21"
}

@techreport{backtrace,
  author = "Ben Liblit and Alex Aiken",
  title = "Building a Better Backtrace: Techniques for Postmortem Program Analysis",
  number = "UCB CSD-02-1203",
  institution = "Computer Science Division, University of California at Berkeley", 
  year = "2002"
}

@techreport{limmat,
  author = "Armin Biere",
  title = "The Evolution from {Limmat} to {Nanosat}",
  number = "444",
  institution = "Dept. of Computer Science, ETH Z\u{u}rich",
  year = "2004"
}

@techreport{QL2,
  author = "R. E. Parr",
  title = "Hierarchical control and learning for {Markov} decision processes",
  year = 1998,
  institution = "University of California, Berkeley",
  number = "PhD thesis"
}

@technicalreport{TR0208,
  author = "A. Groce and W. Visser",
  title = "What Went Wrong:  Explaining Counterexamples",
  number = "02-08",
  institution = "RIACS",
  year = "2002",
}

@technicalreport{DarkoEval,
  author = "Darko Marinov and A. Andoni and D. Daniliuc and Sarfraz Khurshid and Martin Rinard",
  title = "An evaluation of exhaustive testing for data structures",
  number = "MIT-LCS-TR-921",
  institution = "MIT Computer Science and Artificial Intelligence Lab",
  year = 2003
}

@technicalreport{Mota,
  author = "E. Mota and W de Oliveira and J. Kanda",
  title = "Specification and Verification Supported by {AI}:  a new Technological Era",
  number = "RT-03/2002",
  institution = "EsVIA",
  year = "2003"
}



@inproceedings{SympCause,
  author = "T. Ball and M. Naik and S. Rajamani",
  title = "From Symptom to Cause:  Localizing Errors in Counterexample Traces",
  booktitle = "Principles of Programming Languages",
  year = "2003",
  pages = "97--105"
}

@inproceedings{NearNeighbor,
  author = "M. Renieris and S. Reiss",
  title = "Fault Localization With Nearest Neighbor Queries",
  booktitle = "Automated Software Engineering",
  year = "2003"
}

@inproceedings{pdg,
  author = "S. Horwitz and T. Reps",
  title = "The Use of Program Dependence Graphs in Software Engineering.",
  booktitle = "International Conference of Software Engineering",
  year = "1992",
  pages = "392--411"
}


@article{STTTHeur,
  author = "Alex Groce and Willem Visser",
  title = "Heuristics for model checking {Java} programs",
  journal = "Software Tools for Technology Transfer",
  volume = "6(4)",
  year = 2004,
  pages = "260--276"
}

@article{Bowring,
  author = "James Bowring and James Rehg and Mary Jean Harrold",
  title = "Active learning for automatic classification of software behavior",
  booktitle = "International Symposium on Software Testing and Analysis",
  year = 2004,
  pages = "195--205"
}

@inproceedings{Brun,
  author = "Yuriy Brun and Michael Ernst",
  title = "Finding Latent Code Errors via Machine Learning over Program Execution",
  year = 2004,
  booktitle = "International Conference on Software Engineering",
  pages = "480--490"
}

@inproceedings{Tarantula,
  author = "James A. Jones and Mary Jean Harrold",
  title = "Empirical evaluation of the tarantula automatic fault-localization technique",
  booktitle = "Automated Software Engineering",
  pages = "273--282",
  year = 2005
}

@article{Siemens,
  author = "G. Rothermel and M. J. Harrold",
  title = "Empirical Studies of a Safe Regression Test Selection Technique",
  journal = "Software Engineering",
  volume = "24(6)",
  year = "1999",
  pages = "401--419"
}

@inproceedings{TempQuery,
  author = "W. Chan",
  title = "Temporal-logic queries",
  booktitle = "Computer-Aided Verification",
  year = "2000",
  pages = "450--463"
}

@inproceedings{ModelQuery,
  author = "A. Gurfinkel and B. Devereux and M. Chechik",
  title = "Model exploration with temporal logic query checking",
  booktitle = "Foundations of Software Engineering",
  year = "2002",
  pages = "139--148"
}

@inproceedings{StructHeur,
  author = "Alex Groce and Willem Visser",
  title = "Model Checking {Java} Programs using Structural Heuristics",
  booktitle = "International Symposium on Software Testing and Analysis", 
  year = "2002",
  pages = "12--21"
}


@inproceedings{ModelFile,
  author = "J. Yang and P. Twohey and D. Engler and and M. Musuvathi",
  title = "Using Model Checking to Find Serious File System Errors",
  booktitle = "Operating System Design and Implementation",
  year = "2004",
  pages = "273--288"
}

@book{SPIN,
  author="Gerard J. Holzmann",
  title="The {SPIN} Model Checker: Primer and Reference Manual",
  publisher="Addison-Wesley Professional",
  year="2003"}


@inproceedings{SLAM,
  author = "T. Ball and S. Rajamani",
  title = "Automatically Validating Temporal Safety Properties of Interfaces",
  booktitle = "SPIN Workshop on Model Checking of Software",
  year = "2001",
  pages = "103--122"
}

@article{cate,
  author = "Thomas J. Ostrand and Marc J. Balcer",
  title = "The Category-Partition Method for Specifying and Generating Functional Tests",
  year = 1988,
  journal = "Communications of the ACM",
  volume = 31,
  number = 6,
  pages = "676--686"
}

@inproceedings{IsolThread,
  author = "J. Choi and A. Zeller",
  title = "Isolating Failure-Inducing Thread Schedules",
  booktitle = "International Symposium on Software Testing and Analysis",
  year = "2002",
  pages = "210--220"
}

@inproceedings{Mut2000,
  author = "J. Offutt and A. Abdurazik",
  year = 2000,
  booktitle = "Mutation 2000:  Mutation Testing in the Twentieth and the Twenty First Centuries"
}

@article{MutComp,
  author = "R. Hamlet",
  title = "Testing programs with the aid of a compiler",
  year = 1977,
  month = jul,
  journal = "IEEE Transactions on Software Engineering",
  volume = 3,
  number = 4
}

@article{PracProg,
  author = "R. A. DeMillo and R. J. Lipton and F. G. Sayward",
  title = "Hints on test data selection:  Help for the practicing programmer",
  journal = "Computer",
  year = 1978,
  month = apr,
  volume = 4,
  number = 11
}

@inproceedings{BallPred,
  title = "A theory of predicate-complete test coverage and generation",
  author = "Thomas Ball",
  booktitle = "Formal Methods for Components and Objects",
  pages = "1--22",
  year = 2004
}

@misc{JUnit,
  title = "{JUnit}",
  howpublished = "\url{http://junit.sourceforce.net}"
}

@misc{ABPLib,
  title = "Adapatation-Based Programming Library in {Java}",
  howpublished = "\url{http://groups.engr.oregonstate.edu/abp/}"
}

@misc{challenger,
  title = "Report of the Presidential Comission on the Space Shuttle {Challenger} Accident",
  howpublished  = "\url{http://history.nasa.gov/rogersrep/51lcover.htm}"
}

@misc{lars,
  howpublished = "\url{http://eis.jpl.nasa.gov/lars}"
}

@inproceedings{CIL,
  author = "George Necula and Scott McPeak and Shree P. Rahul and Westley Weimer",
  title = "{CIL}: Intermediate Language and Tools for Analysis and Transformation of {C} Programs",
  booktitle = "International Conference on Compiler Construction",
  year = "2002",
  pages = "213--228"
}

@book{CLR,
  author = "Thomas Cormen and Charles Leiserson and Ronald Rivest and Clifford Stein",
  title = "Introduction to Algorithms: Second Edition",
  year = 2001,
  publisher = "MIT Press"
}

@book{Weiss, 
  author = "Mark Allen Weiss",
  title = "Data Structures and Algorithm Analysis in {Java}",
  year = 1998,
  pubilshed = "Addisen Wesley"
}

@unpublished{ACL2Flash,
  author = "J. Erickson and R. Joshi",
  title = "Proving Correctness of a {Flash} Filesystem in {ACL2}",
  year = "2006",
  note = "Unpublished manuscript in preparation"
}

@unpublished{KnuthBugs,
  author = "D. Knuth",
  title = "Notes on the van {Emde Boas} construction of priority deques:  {An} instructive use of recursion",
  year = "1977",
  note = "Letter to Peter van Emde Boas"
}

@unpublished{SelPred,
  author = "N. Dodoo and A. Donovan and L. Lin and M. Ernst",
  title =  "Selecting Predicates for Implications in Program Analysis",
  url = 
  "http://pag.lcs.mit.edu/~mernst/pubs/invariants-implications-abstract.html",
  year = "2000",
  note = "\url{http://pag.lcs.mit.edu/~mernst/pubs/invariants-implications.ps}",
  viewed =  "September 6th, 2002"
}

@inproceedings{DBB,
 author = {Baudry, Benoit and Fleurey, Franck and Le Traon, Yves},
 title = {Improving test suites for efficient fault localization},
 booktitle = {International Conference on Software Engineering},
 year = {2006},
 isbn = {1-59593-375-1},
 pages = {82--91},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1134285.1134299},
 doi = {10.1145/1134285.1134299},
 acmid = {1134299},
 keywords = {diagnosis, mutation analysis, test generation},
} 

@inproceedings{Daikon,
  author = "Michael Ernst and Jake Cockrell and William Griswold and David Notkin",
  title = "Dynamically Discovering Likely Program Invariants to Support Program Evolution",
  booktitle = "Int. Conference on Software Engineering", 
  pages = "213--224",
  year = "1999"
}

@inproceedings{AssumGen,
  author = "D. Giannakopoulou and C. P\u{a}s\u{a}reanu and H. Barringer",
  title = "Assumption Generation for Software Component Verification",
  booktitle = "Automated Software Engineering",
  year = "2002",
  pages = "3--12"
}

@inproceedings{RandFormal,
  author = "Andrea Arcuri and Muhammad Zohaib Z. Iqbal and Lionel C. Briand",
  title = "Formal Analysis of the effectiveness and predictability of random testing",
  year = 2010,
  booktitle = "International Symposium on Software Testing and Analysis",
  pages = "219--230"
}

@inproceedings{RemoteAgent,
  author = "K. Havelund and M. Lowry and S. Park and C. Pecheur and J. Penix and W. Visser and J. White",
  title = "Formal Analysis of the Remote Agent Before and After Flight",
  booktitle = "Proceedings of the 5th NASA Langley Formal Methods  Workshop", 
  year = "2000"
}

@inproceedings{MAGIC,
  author = "S. Chaki and E. Clarke and A. Groce and  S. Jha and H. Veith",
  title = "Modular Verification of Software Components in {C}",
  booktitle = "International Conference on Software Engineering",
  year = "2003",
  pages = "385--395"
}

@inproceedings{DynSlice,
  author = "X. Zhang and R. Gupta and Y. Zhang",
  title = "Precise Dynamic Slicing Algorithms",
  booktitle = "International Conference on Software Engineering",
  year = "2003",
  pages = "319--329"
}

@inproceedings{SymExCrit,
  author = "A Coen-Porisini and G. Denaro and C. Ghezzi and M. Pezze",
  title = "Using Symbolic Execution for Verifying Safety-Critical Systems",
  booktitle = "European Software Engineering Conference/Foundations of Software Engineering",
  year = "2001",
  pages = "142--151"
}


@inproceedings{CountWitness,
  author = "E. Clarke and O. Grumberg and K. McMillan and X. Zhao",
  title = "Efficient generation of counterexamples and witnesses in symbolic model checking",
  booktitle = "Design Automation Conference",
  year = "1995",
  pages = "427--432"
}

@inproceedings {BLASTLazy,
  author = "Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and Gregoire Sutre",
  title = "Lazy Abstraction",
  booktitle = "Principles of Programming Languages",
  year = "2002",
  pages = "58--70"
}

@inproceedings{FreeWill,
  author = "H. Jin and K. Ravi and F. Somenzi",
  title = "Fate and Free Will in Error Traces",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
  pages = "445--458",
  year = "2002"
}

@inproceedings{ProofLike,
  author = "M. Chechik and A. Gurfinkel",
  title = "Proof-Like Counter-Examples",
  booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
  year = "2003",
  pages = "160--175"
}

@inproceedings{EvidenceBased,
  author = "L. Tan and R. Cleaveland",
  title = "Evidence-Based Model Checking",
  booktitle = "Computer-Aided Verification",
  year = "2002",
  pages = "455--470"
}

@inproceedings{DEOS,
  author = "J. Penix and W. Visser and E. Engstrom and A. Larson and N.  Weininger",
  title = "Verification of Time Partitioning in the {DEOS} Scheduler Kernel",
  booktitle = "International Conference on Software Engineering", 
  pages = "488--497",
  year = "2000"
}

@inproceedings{TestVer,
  author = "N. Sharygina and D. Peled",
  title = "A Combined Testing and Verification Approach for Software Reliability",
  booktitle = "Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe",
  pages = "611--628",
  year = "2001"
}

@inproceedings{WhiteBox,
  author = "Patrice Godefroid and Michael Y. Levin and David A. Molnar",
  title = "Automated Whitebox Fuzz Testing",
  year = 2008,
  booktitle = "Proceedings of the Network and Distributed System Security Symposium"
}

@inproceedings{csmith,
  author = "Xuejun Yang and Yang Chen and Eric Eide and John Regehr",
  title = "Finding and Understanding Bugs in {C} Compilers",
  booktitle = "ACM SIGPLAN Conference on Programming Language Design and Implementation",
  year = 2011,
  pages = "283--294"
}

@article{swarmIEEE,
  author = "Gerard Holzmann and Rajeev Joshi and Alex Groce",
  title = "Swarm Verification Techniques",
  journal = "IEEE Transactions on Software Engineering",
volume = {37},
number = {6},
  year = 2011,
  pages = "845--857"
}

@inproceedings{XuMG08,
  author    = {Ru-Gang Xu and
               Rupak Majumdar and
	       Patrice Godefroid},
  title     = {Testing for Buffer Overflows with Length Abstraction},
  booktitle = {International Symposium on Software Testing and Analysis},

  year      = {2008},
  pages = "19--28"
}


@inproceedings{swarmVer,
  author = "Gerard Holzmann and Rajeev Joshi and Alex Groce",
  title = "Swarm Verification",
  booktitle = "Automated Software Engineering",
  year = 2008,
  pages = "1--6"
}

@inproceedings{swarm,
  author = "Gerard Holzmann and Rajeev Joshi and Alex Groce",
  title = "Tackling Large Verification Problems with the Swarm Tool",
  booktitle = "SPIN Workshop on Model Checking of Software",
  year = 2008,
  pages = "134--143"
}

@inproceedings{SMART,
  author = {Patrice Godefroid},
  title = "Compositional dynamic test generation",
  year = 2007,
  booktitle = "Principles of Programming Languages",
  pages = "47--54"
}

@misc{jsfunfuzz,
  title = "Introducing jsfunfuzz",
  year = 2007,
  note = "\url{http://www.squarefree.com/2007/08/02/introducing-jsfunfuzz/}",
  author = "Jesse Ruderman"
}

@misc{JPF,
  title = "{JPF}: the swiss army knife of {Java(TM)} verification",
  howpublished = "\url{http://babelfish.arc.nasa.gov/trac/jpf}"
}

@inproceedings{sglib,
  author =       "Marian Vittek and Peter Borovansky and Pierre-Etienne Moreau",
  title =        "A Simple Generic Library for {C}",
  year =         "2006",
  pages =        "423-426",
  booktitle =    {Int. Conference on Software Reuse}
}

@misc{lobo,
  title = "The {Lobo} Project",
  howpublished = "\url{http://lobobrowser.org}"
}

@misc{CREST,
  title = "{CREST}: automatic test generation tool for {C}",
  howpublished = "\url{http://code.coogle.com/p/crest}"
}

@inproceedings{GodefroidKS05,
  author    = {Patrice Godefroid and
               Nils Klarlund and
               Koushik Sen},
  title     = {{DART:} directed automated random testing},
  booktitle = {Programming Language Design and Implementation},
  pages = "213--223",
  year      = {2005}
}

@article{MLGlossary,
  title = "Glossary of Terms",
  journal = "Journal of Machine Learning",
  year = 1998,
  volume = 30,
  pages = "271--274",
  author = "Ron Kohavi and Foster Provost"
}

@inproceedings{SenMA05,
  author    = {Koushik Sen and
               Darko Marinov and
               Gul Agha},
  title     = {{CUTE:} a concolic unit testing engine for {C}},
  booktitle = {Foundations of Software Engineering},
  pages = "262--272",
  year      = {2005}
}

@inproceedings{CFV08,
  author = "Alex Groce and Gerard Holzmann and Rajeev Joshi and Ru-Gang Xu",
  title = "Putting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving",
  booktitle = "Workshop on Constraints in Formal Verification",
  pages = "1--15",
  year = 2008
}

@book{ReinforceBook,
  author = "Richard Sutton and Andrew Barto",
  title = "Reinforcement Learning: an Introduction",
  year = 1998,
  publisher = "MIT Press"
}

@inproceedings{CadarGPDE06,
  author    = {Cristian Cadar and
               Vijay Ganesh and
               Peter Pawlowski and
               David Dill and
               Dawson Engler},
  title     = {{EXE:} automatically generating inputs of death},
  booktitle = {Conference on Computer and Communications Security},
  pages = "322--335",
  year      = {2006}
}

@inproceedings{codesurfer,
  author = "P. Anderson and T. Teitelbaum",
  title = "Software inspection using codesurfer",
  booktitle = "Workshop on Inspection in Software Engineering",
  year = "2001"
}

@inproceedings{Autopilot,
  author = "O. Tkachuk and G. Brat and W. Visser",
  title = "Using Code Level Model Checking To Discover Automation Surprises",
  booktitle = "Digital Avionics Systems Conference",
  year = "2002"
}

@inproceedings{WODA08,
  author = "Alex Groce and Rajeev Joshi",
  title = "Random Testing and Model Checking:  Building a Common Framework for Nondeterministic Exploration",
  booktitle = "Workshop on Dynamic Analysis",
  pages = "22--28",
  year = 2008
}

@inproceedings{MiniChall,
  author = "Rajeev Joshi and Gerard Holzmann",
  title = "A Mini-Challenge: Build A Verifiable Filesystem",
  booktitle = "The Conference on Verified Software:  Theories, Tools, Experiments",
  year = 2005
}

@inproceedings{Malicious,
  author = "Junfeng Yang and Can Sar and Paul Twohey and Cristian Cadar and Dawson Engler",
  title = "Automatically Generating Malicious Disks using Symbolic Execution",
  booktitle = "IEEE Symposium on Security and Privacy",
  year = "2006",
  pages = "243--257"
}

@inproceedings{StorageError,
  author = "Junfeng Yang and Can Sar and Dawson Engler",
  title = "{EXPLODE:} A Lightweight, General System for Finding Serious Storage System Errors",
  booktitle = "Operating System Design and Implementation",
  year = "2006",
  pages = "131--146"
}

@inproceedings{KimSPIN,
  author = "Moonzoo Kim and Yunja Choi and Yunho Kim and Hotae Kim",
  title = "Formal Verification of a Flash Memory Device Driver --- an Experience Report",
  booktitle = "SPIN Workshop on Model Checking of Software",
  year = 2008,
  pages = "144--159"
}

@inproceedings{KimASE,
  author = "Moonzoo Kim and Yunho Kim and Hotae Kim",
  title = "Unit Testing of Flash Memory Device Driver through a {SAT}-Based Model Checker",
  booktitle = "Automated Software Engineering",
  year = 2008,
  pages = "198--207"
}

@inproceedings{KimICST,
  author = "Moonzoo Kim and Yunja Choi and Yunho Kim and Hotae Kim",
  title = "Pre-testing Flash Device Driver through Model Checking Techniques",
  booktitle = "International Conference on Software Testing, Verification, and Validation",
  year = 2008,
  pages = "475--484"
}


@inproceedings{WODA09,
  author = "Alex Groce",
  title = "({Quickly}) Testing the Tester via Path Coverage",
  booktitle = "Workshop on Dynamic Analysis",
  year = 2009
}

@inproceedings{PathSensitive,
  author = "Matthew B. Dwyer and Suzette Person and Sebastian Elbaum",
  title = "Controlling factors in evaluating path-sensitive error detection techniques",
  booktitle = "Foundations of Software Engineering",
  year = 2006,
  pages = "92--104"
}

@inproceedings{JPFRandTest,
  author = "Willem Visser and Corina P\u{a}s\u{a}reanu and Radek Pelanek",
  title = "Test Input Generation for {Java} containers using state matching",
  booktitle = "International Symposium on Software Testing and Analysis",
  year = "2006",
  pages = "37--48"
}

@article{JPF2,
  author = "Willem Visser and Klaus Havelund and Guillaume Brat and SeungJoon Park and Flavio Lerda",
  title = "Model Checking Programs",
  journal = "Automated Software Engineering",
  volume = "10",
  number = "2",
  year = "2003",
  month = apr,
  pages = "203--232"
}

@inproceedings{RyderExcept,
  author = "Chen Fu and Ryder, Barbara",
  title = "Exception-Chain Analysis: Revealing Exception Handling Architecture in Java Server Applications",
  year = 2007,
  booktitle = "International Conference on Software Engineering",
  pages = "230--239"
}

@techreport{AndrewsTR,
  author = "Jamie Andrews and Yihao Ross Zhang and Alex Groce",
  title = "Comparing Automated Unit Testing Strategies",
  institution = "Department of Computer Science, University of Western Ontario",
  month = "December",
  year = 2010,
  number = 736
}

@techreport{tassey-nist,
	author = {Tassey, Gregory},
	citeulike-article-id = {3450366},
	citeulike-linkout-0 = {http://www.nist.gov/director/prog-ofc/report02-3.pdf},
	institution = {National Institute of Standards and Technology},
	keywords = {debugging, programming},
	month = may,
	posted-at = {2008-10-25 16:49:19},
	priority = {2},
	title = {The Economic Impacts of Inadequate Infrastructure for Software Testing},
	url = {http://www.nist.gov/director/prog-ofc/report02-3.pdf},
	year = {2002}
}

@techreport{posix,
	booktitle = {IEEE Std 1003.1, 2004 Edition. The Open Group Technical Standard. Base Specifications, Issue 6. Includes IEEE Std 1003.1-2001, IEEE Std 1003.1-2001/Cor 1-2002 and IEEE Std 1003.1-2001/Cor 2-2004. Shell and Utilities},
	citeulike-article-id = {1577260},
	citeulike-linkout-0 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1309816},
	journal = {IEEE Std 1003.1, 2004 Edition. The Open Group Technical Standard. Base Specifications, Issue 6. Includes IEEE Std 1003.1-2001, IEEE Std 1003.1-2001/Cor 1-2002 and IEEE Std 1003.1-2001/Cor 2-2004. Shell and Utilities},
	keywords = {ieee, operating, posix, shell, specification, system, systems, thread, threaded, threads, unix},
	posted-at = {2008-06-18 10:50:13},
	priority = {0},
	title = {Standard for information technology - portable operating system interface ({POSIX}). {Shell} and utilities},
	url = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1309816},
	year = {2004}
}

@inproceedings{EvalAssoc,
  author = "David Lo Lucia and Lingxiao Jiang and Aditya Budi",
  title = "Comprehensive Evaluation of Association Measures for Fault Localization",
  booktitle = "International Conference on Software Maintenance",
  year = 2010,
  pages = "1--10"
}

@misc{CodeCover, 
title = "{CodeCover} - an open-source glass-box testing tool",
howpublished = "\url{http://codecover.org/}"}

@misc{OSUPlatform, howpublished = "\url{http://eecs.oregonstate.edu/education/cspfl/index.php}"}

@misc{xie, howpublished = "\url{http://research.csc.ncsu.edu/ase/courses/csc712/2008fall/}"}

@misc{caltech, howpublished = "\url{http://www.cs.cmu.edu/~agroce/CS119}"}

@inproceedings{OSUPlat,
  author = "Carlos Jensen and Eric Betts and Yunrim Park and Don Heer and Kevin Kemper and Ben Goska",
  title = "Building a {CS} Platform for Learning: An Open Source Approach",
  booktitle = "Integrating FOSS into the Undergraduate Computing Curriculum:  Free and Open Source Software (FOSS) Symposium",
  year = 2009
}

@misc{marinov, howpublished = "\url{https://agora.cs.illinois.edu/display/cs498dmsp09/Home}"}

@misc{CBMC,
  howpublished = "\url{http://www.cs.cmu.edu/~modelcheck/cbmc/}"
}

@misc{MSL,
  howpublished = "\url{http://mars.jpl.nasa.gov/msl/}"
}

@misc{EVRJPL,
  howpublished = "\url{http://stardust.jpl.nasa.gov/news/acronims.htm}"
}

@inproceedings{Heimdahl,
  title = "Auto-generating test sequences using model checkers:  A case study",
  author = "M. P. E. Heimdahl and S Rayadurgam and W. Visser and D. George and J. Gao",
  booktitle = "International Workshop on Formal Approaches to Testing of Software (FATES)",
  year = 2003
}

@inproceedings{NewChall,
  author = "Gerard Holzmann and Rajeev Joshi and Alex Groce",
  title = "New Challenges in Model Checking",
  booktitle = "Symposium on 25 Years of Model Checking",
  year = 2008,
  pages = "65--76"
}

@inproceedings{CauseEffect,
  author = "A. Zeller",
  title = "Isolating Cause-Effect Chains from Computer Programs",
  booktitle = "Foundations of Software Engineering",
  year = "2002",
  pages = "1--10"
}

@inproceedings{TestsFromCEs,
  author = "D. Beyer and A. J. Chlipala and T. A. Henzinger and R. Jhala and R. Majumdar",
  booktitle = "International Conference on Software Engineering",
  year = 2004,
  title = "Generating tests from counterexamples",
  pages = "326--335"
}

@inproceedings{DynamicSlicing,
  author = "Hiralal Agrawal and Jospeh R. Horgan",
  title = "Dynamic program slicing",
  booktitle = "Programming Language Design and Implementation",
  year = "1990",
  pages = "246--256"
}

@article{Tip,
    author = "Frank Tip",
    title = "A survey of program slicing techniques",
    journal = "Journal of programming languages",
    volume = "3",
    pages = "121--189",
    year = "1995"
}

@inproceedings{AutoAuto,
  author = "R. Simmons and C. Pecheur",
  title = "Automating Model Checking for Autonomous Systems",
  booktitle = "AAAI Spring Symposium on Real-Time Autonomous Systems",
  year = "2000"
}

@inproceedings{scriptstospecs,
  author = "Alex Groce and Klaus Havelund and Margaret Smith",
  title = "From Scripts to Specifications:  The Evolution of a Flight Software Testing Effort",  
  booktitle = "International Conference on Software Engineering",
  year = 2010,
  pages = "129--138"
}

@article{Differential,
  author = "William McKeeman",
  title = "Differential testing for software",
  journal = "Digital Technical Journal of Digital Equipment Corporation",
  volume = "10(1)",
  pages = "100--107",
  year = 1998
}

@article{Isolating,
  author = "Andreas Zeller and Ralf Hildebrandt",
  title = "Simplifying and Isolating Failure-Inducing Input",
  journal = "IEEE Trans. on Software Engineering",
  volume = "28(2)",
  year = "2002",
  pages = "183--200"
}

@book{TestDriven,
  title = "Test Driven Development:  By Example",
  year = 2002,
  publisher = "Addison Wesley",
  author = "Kent Beck"
}

@book{OffuttBook,
  author = "Paul Ammann and Jeff Offutt",
  title = "Introduction to Software Testing",
  publisher = "Cambridge University Press",
  year = 2008
}

@book{Beizer,
  author = "Boris Beizer",
  title = "Software Testing Techniques",
  publisher = "International Thomson Computer Press",
  year = 1990
}

@book{pezze,
  author = "Mauro Pezze and Michal Young",
  title = "Software Testing and Analysis:  Process, Principles, and Techniques",
  publisher = "John Wiley and Sons",
  year = "2008"
}


@book{kidder,
   author = "Tracy Kidder",
   title = "The Soul of a New Machine",
   year = 1981,
   publisher = "Little, Brown"
}

@book{EWD:Discipline,
  AUTHOR =       {Edsger W. Dijkstra},
  TITLE =        {A {D}iscipline of {P}rogramming},
  PUBLISHER =    {Prentice-Hall, Englewood Cliffs, New Jersey},
  YEAR =         {1976}
}

@inproceedings{ESCJ,
  author =       {Cormac Flanagan and K. Rustan M. Leino and Mark Lillibridge and Greg Nelson and James B. Saxe and Raymie Stata},
  title =        {Extended static checking for {J}ava},
  booktitle =    {Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)},
  pages =        "234--245",
  month =        may,
  year =         2002
}

@article{Leino:EfficientWP,
  author =       {K. Rustan M. Leino},
  title =        {Efficient weakest preconditions},
  journal =      {Information Processing Letters},
  volume =       "93(6)",
  year =         2005
}

@article{king,
  author = "J. C. King",
  title = "Symbolic execution and program testing",
  journal = "Communications of the ACM",
  year = 1976,
  volume = 19,
  number = 7
}

@inproceedings{FlanaganSaxe:Explosion,
  author =       {Cormac Flanagan and James B. Saxe},
  title =        {Avoiding exponential explosion: {G}enerating compact verification conditions},
  booktitle =    "Principles of Programming Languages",
  pages =        "193--205",
  year =         "2002"
}

@BOOK{DijkstraScholten:Book,
  AUTHOR =       {Edsger W. Dijkstra and C. S. Scholten},
  TITLE =        {Predicate Calculus and Program Semantics},
  PUBLISHER =    {Springer-Verlag},
  SERIES =       {Texts and Monographs in Computer Science},
  YEAR =         {1990}
}

@misc{Flash,
  title =        {A Collection of {NAND} {Flash} Application Notes, Whitepapers and Articles},
  howpublished =       {\url{http://www.data-io.com/NAND/NANDApplicationNotes.asp}}
}


@article{Lowe95,
  author    = {Gavin Lowe},
  title     = {An Attack on the {Needham}-{Schroeder} Public-Key Authentication
               Protocol},
  journal   = {Information Processing Letters},
  volume    = {56},
  number    = {3},
  year      = {1995},
  pages     = {131--133},
  ee        = {http://dx.doi.org/10.1016/0020-0190(95)00144-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{NeedhamS78,
  author    = {Roger M. Needham and
               Michael D. Schroeder},
  title     = {Using Encryption for Authentication in Large Networks of
               Computers},
  journal   = {Communications of the ACM},
  volume    = {21},
  number    = {12},
  year      = {1978},
  pages     = {993--999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book { taylor-karlin-book,
  author	= {Howard M. Taylor and Samuel Karlin},
  title		= {An introduction to stochastic modeling},
  edition	= 3,
  address	= {San Diego},
  publisher	= {Academic Press},
  year		= 1998
}

@INPROCEEDINGS
(
  andrews-etal-rute-rt,
  author        = {James H. Andrews and Susmita Haldar and Yong Lei
                   and Chun Hang Felix Li},
  title         = {Tool Support for Randomized Unit Testing},
  booktitle     = {Proceedings of the First International Workshop on
                   Randomized Testing},
  address       = {Portland, Maine},
  month         = jul,
  year          = 2006,
  pages         = {36--45}
)

@article{Ortho,
  author = "M. S. Phadke",
  title = "Planning Efficient Software Tests",
  year = 1997,
  journal = "CrossTalk",
  number = 10,
  volume = 10,
  pages = "11--15",
  month = oct
}

@inproceedings{mutant,
  author = "James H. Andrews and L. C. Briand and Y. Labiche",
  title = "Is Mutation an Appropriate Tool for Testing Experiments?",
  year = 2005,
  booktitle = "International Conference on Software Engineering",
  pages = "402--411"
}

@inproceedings{ASE08,
  author = "James H. Andrews and Alex Groce and Melissa Weston and Ru-Gang Xu",
  title = "Random Test Run Length and Effectiveness",
  booktitle = "Automated Software Engineering",
pages = "19--28",
  year = 2008
}

@article{part,
  author = "R. Hamlet and R. Taylor",
  title = "Partition testing does not inspire confidence",
  journal = "IEEE Transactions on Software Engineering",
  year = 1990,
  volume = 16,
  number = 12,
  pages = "1402--1411"
}

@article{evalrand,
  author = "J. W. Duran and S. C. Ntafos",
  title = "Evaluation of random testing",
  journal = "IEEE Transactions on Software Engineering",
  volume = 10,
  number = 4,
  pages = "438--444",
  year = 1984
}

@ARTICLE
(
  doong-frankl-tosem94,
  author        = {Roong-Ko Doong and Phyllis G. Frankl},
  title         = {The {ASTOOT} Approach to Testing Object-Oriented Programs},
  journal       = {ACM Transactions on Software Engineering and Methodology},
  volume        = 3,
  number        = 2,
  pages         = {101--130},
  month         = apr,
  year          = 1994
)

